호모토피 타입 이론

호모토피 타입 이론(Homotopy type theory, HoTT)은 호모토피 이론적 시각에 기반한 타입 이론이다. 마틴뢰프 타입 이론의 일종이다.

타입과 위상 공간

HoTT에서 타입은 위상 공간으로, 타입의 원소들을 위상 공간의 점으로 해석된다. 즉 \(a : A\)는 "\(a\)는 위상 공간 \(A\)의 점이다"를 의미한다.

호모토피 레벨

h-명제

h-명제는 전통적인 명제처럼 행동하는 타입이다. proof irrelevance가 성립하는 타입으로 정의된다. \[ \newcommand{\isProp}[0] {\operatorname{isProp}} \isProp(A) \triangleq \prod_{x,y:A} x = y \]

h-집합

h-집합은 전통적인 집합처럼 행동하는 타입이다. h-집합은 동일성이 h-명제인 타입으로 다음과 같이 정의된다. \[ \newcommand{\isSet}[0] {\operatorname{isSet}} \isSet(A) \triangleq \prod_{x,y:A} \isProp(x = y) \]

h-준군

h-준군은 준군처럼 행동하는 타입이다. 다음과 같이 정의된다. \[ \newcommand{\isGroupoid}[0] {\operatorname{isGroupoid}} \isGroupoid(A) \triangleq \prod_{x,y:A} \isSet(x = y) \]

축약 가능한 타입과 일반화

일반적으로 이러한 과정을 무한히 반복할 수 있다. \[ \newcommand{\isTwoGroupoid}[0] {\operatorname{is2Groupoid}} \newcommand{\isThreeGroupoid}[0] {\operatorname{is3Groupoid}} \begin{array}{l} \isTwoGroupoid(A) \triangleq \displaystyle\prod_{x,y:A} \isGroupoid(x = y) \\ \isThreeGroupoid(A) \triangleq \displaystyle\prod_{x,y:A} \isTwoGroupoid(x = y) \\ \ldots \end{array} \]

또한, 이 과정을 반대로도 진행 할 수 있다. 축약 가능한 타입을 다음과 같이 정의한다. \[ \newcommand{\isContr}[0] {\operatorname{isContr}} \isContr(A) \triangleq \sum_{x:A} \prod_{y:A} x = y \\ \]

이때 다음이 성립한다. \[ \isProp(A) \ \ \text{iff} \ \prod_{x,y:A} \isContr(x = y) \]

타입 \(A\)가 h-레벨 \(n\)을 가짐을 의미하는 명제를 \(\operatorname{isOfHLevel}(n,A)\)라고 쓰고, 다음과 같이 정의한다. \[ \newcommand{\isOfHLevel}[0] {\operatorname{isOfHLevel}} \begin{array}{ll} \isOfHLevel(0, A) &\triangleq \isContr(A) \\ \isOfHLevel(1+n, A) &\triangleq \displaystyle\prod_{x,y:A} \isOfHLevel(n,x=y) \end{array} \]